﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.SimpleStack
{
    [PexClass(typeof(SimpleStack))]    
    public partial class SimpleStackTest
    {
        /// <summary>
        /// An easy target to achieve which can be done by just a sequence of method calls
        /// </summary>
        /// <param name="st"></param>
        [PexAssertReachEventually]
        [PexMethod]
        public void StackSizePUT([PexAssumeUnderTest]SimpleStack st)
        {
            int k = 10;
            if (st.Size() > k)
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// A difficult target, along with size, a specific element needs to be 
        /// </summary>
        /// <param name="st"></param>
        [PexAssertReachEventually]
        [PexMethod]
        public void StackTopElementPUT([PexAssumeUnderTest]SimpleStack st)
        {
            if (st.Pop() == 20 && st.Size() == 10)
                PexAssert.ReachEventually();
        }

        [PexMethod]
        public void StackNotPUTTest([PexAssumeUnderTest]SimpleStack st)
        {
            st.Push(10);
        }

        [PexMethod]
        public void TestMethod(int i)
        {
            if (i > 0)
                PexAssert.IsFalse(true);

        }
    }
}
